\begin{tabbing}
$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:ecl(${\it ds}$;${\it da}$), $L$:event{-}info(${\it ds}$;${\it da}$) List.
\\[0ex]ecl{-}trans{-}normal(ecl{-}trans($x$))
\\[0ex]\& ($\forall$$n$:$\mathbb{N}^{+}$. ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;ecl{-}trans($x$))($n$,$L$) $\Rightarrow$ ($n$ $\in$ ecl{-}trans{-}es(ecl{-}trans($x$))))
\\[0ex]\& (\=$\forall$$n$:$\mathbb{N}$.\+
\\[0ex]($\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ \& ecl{-}halt(${\it ds}$;${\it da}$;$x$)($n$,${\it L'}$))
\\[0ex]$\Leftrightarrow$
\\[0ex]ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;ecl{-}trans($x$))($n$,$L$))
\-\\[0ex]\& ($\forall$$m$:$\mathbb{N}$. ecl{-}act(${\it ds}$;${\it da}$;$m$;$x$)($L$) $\Leftrightarrow$ ecl{-}trans{-}act(${\it ds}$;${\it da}$;ecl{-}trans($x$))($m$,$L$))
\end{tabbing}